T:Type, P1, P2:(T), L:T List. filter(P1;filter(P2;L)) ~ filter(P2;filter(P1;L)) 

latex

Definitions	t  T, type List, x:AB(x), s ~ t, x:A. B(x), , Type, b, A, b, s = t, Prop, f(a), P  Q, x:AB(x), P & Q, P  Q, Unit, left+right, {T}, SQType(T)
Lemmas	not assert elim, bool sq, assert elim, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, bool wf